Thomas Wies

Contact

wies at cs.nyu.edu
+1 (212) 998 3293
60 Fifth Avenue
Room 403
New York, NY 10011

Group Members

Ph.D. Students

Devora Chait-Roth
Mark Goldstein (co-advisor)
Ekanshdeep Gupta
Elaine Li
Jacob Salzberg (co-advisor)

Group Alumni

Kshitij Bansal (co-advisor)
Siddharth Krishna
Chanseok Oh
Zvonimir Pavlinovic
Nisarg Patel
Daniel Schwartz-Narbonne
Yan Shvartzshnaider
Wei Wang (co-advisor)
Sebastian Wolff

Research

My research focuses on program analysis and verification, automated deduction, and concurrency.

Selected Publications

Complete list of publications

Tools

As a byproduct of my research, I have developed and contributed to a number of tools.

  • GRASShopper

    A verification tool that checks functional correctness of programs manipulating heap-allocated data structures.
  • Vermeer

    An automated debugging tool that traces and explains faults in C programs.
  • Picasso

    A static analyzer for depth-bounded concurrent systems. It has been used to verify properties of non-blocking concurrent data structures and distributed message passing algorithms with an unbounded number of threads and messages.

Teaching

Professional Activities

Organizer

Publications

See also my DBLP entry for a complete list of my publications.

Books

  1. Automated Verification of Concurrent Search Structures pdf

    S. Krishna, N. Patel, D. Shasha, and T. Wies
    Morgan & Claypool Publishers, 2021

In Journals

  1. Embedding Hindsight Reasoning in Separation Logic pdf

    R. Meyer, T. Wies, and S. Wolff
    PACMPL, 7(Programming Language Design and Implementation (PLDI)), 2023
  2. A Concurrent Program Logic with a Future and History pdf

    R. Meyer, T. Wies, and S. Wolff
    PACMPL, 6(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2022
  3. Verifying Concurrent Multicopy Search Structures pdf

    N. Patel, S. Krishna, D. Shasha, and T. Wies
    PACMPL, 5(Object-oriented Programming, Systems, Languages, and Applications (OOPSLA)), 2021
  4. Dataflow Refinement Type Inference pdf talk

    Z. Pavlinovic, Y. Su, and T. Wies
    PACMPL, 5(ACM Symposium on the Principles of Programming Languages (POPL)), 2021
  5. Go with the Flow: Compositional Abstractions for Concurrent Data Structures pdf

    S. Krishna, D. Shasha, and T. Wies
    PACMPL, 2(ACM Symposium on the Principles of Programming Languages (POPL)), 2018
  6. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    Journal of Automated Reasoning, 57(1), 2016
  7. Preface - Invariant Generation pdf

    G. Grov and T. Wies
    Science of Computer Programming (SCICO), 93, 2014
  8. Doomed Program Points pdf

    J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies
    Formal Methods in System Design (FMSD), 37(2-3), 2010

In Conferences

  1. Verifying Lock-free Search Structure Templates pdf

    N. Patel, D. Shasha, and T. Wies
    In Proceedings of European Conference on Object-Oriented Programming (ECOOP), 2024
  2. Deciding Subtyping for Asynchronous Multiparty Sessions pdf

    E. Li, F. Stutz, and T. Wies
    In Proceedings of European Symposium on Programming (ESOP), 2024
  3. Complete Multiparty Session Type Projection with Automata pdf

    E. Li, F. Stutz, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2023
  4. nekton: a linearizability proof checker pdf

    R. Meyer, A. Opaterny, T. Wies, and S. Wolff
    In Proceedings of Computer Aided Verification (CAV), 2023
  5. Less is more: refinement proofs for probabilistic proofs pdf

    K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
    In Proceedings of IEEE Symposium on Security and Privacy (IEEE S&P), 2023
  6. Make flows small again: revisiting the flow framework pdf

    R. Meyer, T. Wies, and S. Wolff
    In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023
  7. Needles in a Haystack: Using PORT to Catch Bad Behaviors within Application Recordings pdf

    P. Moore, T. Wies, M. Waldman, P. Frankl, and J. Cappos
    In Proceedings of International Conference on Software Technologies (ICSOFT), 2022
  8. Inverse-Weighted Survival Games pdf

    M. Goldstein, X. Han, A.M. Puli, T. Wies, A.J. Perotte, and R. Ranganath
    In Proceedings of Conference on Neural Information Processing Systems (NeurIPS), 2021
  9. TarTar: A Timed Automata Repair Tool pdf

    M. Kölbl, S. Leue, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2020
  10. Verifying Concurrent Search Structure Templates pdf talk

    S. Krishna, N. Patel, D. Shasha, and T. Wies
    In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2020
  11. Local Reasoning for Global Graph Properties pdf talk

    S. Krishna, A.J. Summers, and T. Wies
    In Proceedings of European Symposium on Programming (ESOP), 2020
  12. Charting a Course Through Uncertain Environments: SEA Uses Past Problems to Avoid Future Failures pdf Best Paper Award

    P. Moore, J. Cappos, P. Frankl, and T. Wies
    In Proceedings of International Symposium on Software Reliability Engineering (ISSRE), 2019
  13. Clock Bound Repair for Timed Systems pdf

    M. Kölbl, S. Leue, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2019
  14. VACCINE: Using Contextual Integrity for Data Leakage Detection pdf

    Y. Shvartzshnaider, Z. Pavlinovic, A. Balashankar, T. Wies, L. Subramanian, H. Nissenbaum, and P. Mittal
    In Proceedings of World Wide Web Conference (WWW), 2019
  15. Full accounting for verifiable outsourcing pdf

    R. Wahby, Y. Ji, A.J. Blumberg, a. shelat, J. Thaler, M. Walfish, and T. Wies
    In Proceedings of ACM Conference on Computer and Communications Security (CCS), 2017
  16. Partitioned Memory Models for Program Analysis pdf

    W. Wang, C. Barrett, and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2017
  17. Error Invariants for Concurrent Traces pdf

    A. Holzer, D. Schwartz-Narbonne, M. Tabaei, G. Weissenbacher, and T. Wies
    In Proceedings of International Symposium on Formal Methods (FM), 2016
  18. Learning Privacy Expectations by Crowdsourcing Contextual Informational Norms pdf

    Y. Shvartzshnaider, S. Tong, T. Wies, P. Kift, H. Nissenbaum, L. Subramanian, and P. Mittal
    In Proceedings of AAAI Conference on Human Computation and Crowdsourcing (HCOMP), 2016
  19. Classifying Bugs with Interpolants pdf

    A. Podelski, M. Schäf, and T. Wies
    In Proceedings of Tests and Proofs (TAP), 2016
  20. Practical SMT-Based Type Error Localization pdf

    Z. Pavlinovic, T. King, and T. Wies
    In Proceedings of ACM SIGPLAN International Conference on Functional Programming (ICFP), 2015
  21. Deciding Local Theory Extensions via E-Matching pdf

    K. Bansal, T. King, A. Reynolds, C. Barrett, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2015
  22. VERMEER: A Tool for Tracing and Explaining Faulty C Programs pdf

    D. Schwartz-Narbonne, C. Oh, M. Schäf, and T. Wies
    In Proceedings of International Conference on Software Engineering (ICSE), Demonstrations Track, 2015
  23. Conflict-Directed Graph Coverage pdf

    D. Schwartz-Narbonne, M. Schäf, D. Jovanović, P. Rümmer, and T. Wies
    In Proceedings of NASA Formal Methods (NFM), 2015
  24. Finding Minimum Type Error Sources pdf Best Paper Award

    Z. Pavlinovic, T. King, and T. Wies
    In Proceedings of ACM SIGPLAN International Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014
  25. Concolic Fault Abstraction pdf

    C. Oh, M. Schäf, D. Schwartz-Narbonne, and T. Wies
    In Proceedings of IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 2014
  26. Automating Separation Logic with Trees and Data pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2014
  27. Dynamic Package Interfaces pdf

    S. Esmaeilsabzali, R. Majumdar, T. Wies, and D. Zufferey
    In Proceedings of Fundamental Approaches to Software Engineering (FASE), 2014
  28. GRASShopper: Complete Heap Verification with Mixed Specifications pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014
  29. Cascade 2.0 pdf

    W. Wang, C. Barrett, and T. Wies
    In Proceedings of VMCAI, 2014
  30. Explaining Inconsistent Code pdf

    M. Schäf, T. Wies, and D. Schwartz-Narbonne
    In Proceedings of ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2013
  31. Automating Separation Logic using SMT pdf

    R. Piskac, T. Wies, and D. Zufferey
    In Proceedings of Computer Aided Verification (CAV), 2013
  32. Structural Counter Abstraction pdf

    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    In Proceedings of TACAS, 2013
  33. Flow-Sensitive Fault Localization pdf

    J. Christ, E. Ermis, M. Schäf, and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013
  34. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2013
  35. Error Invariants pdf

    E. Ermis, M. Schäf, and T. Wies
    In Proceedings of Formal Methods (FM), 2012
  36. Deciding Functional Lists with Sublist Sets pdf

    T. Wies, M. Muñiz, and V. Kuncak
    In Proceedings of Verified Software: Theories, Tools, Experiments (VSTTE), 2012
  37. Ideal Abstractions for Well-Structured Transition Systems pdf

    D. Zufferey, T. Wies, and T.A. Henzinger
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012
  38. An Efficient Decision Procedure for Imperative Tree Data Structures pdf

    T. Wies, M. Muñiz, and V. Kuncak
    In Proceedings of Conference on Automated Deduction (CADE-23), 2011
  39. Scheduling Large Jobs by Abstraction Refinement pdf

    T.A. Henzinger, V. Singh, T. Wies, and D. Zufferey
    In Proceedings of European Conference on Computer Systems (EuroSys), 2011
  40. Decision Procedures for Automating Termination Proofs pdf

    R. Piskac and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011
  41. A Marketplace for Cloud Computing pdf

    T.A. Henzinger, V. Singh, A. Tomar, T. Wies, and D. Zufferey
    In Proceedings of International Conference on Embedded Systems (EMSOFT), 2010
  42. FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment pdf

    T.A. Henzinger, V. Singh, A. Tomar, T. Wies, and D. Zufferey
    In Proceedings of IEEE International Conference on Cloud Computing (IEEE CLOUD), 2010
  43. Forward Analysis of Depth-Bounded Processes pdf

    T. Wies, D. Zufferey, and T.A. Henzinger
    In Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), 2010
  44. Counterexample-guided focus pdf slides

    A. Podelski and T. Wies
    In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2010
  45. Building a Calculus of Data Structures pdf

    V. Kuncak, R. Piskac, P. Suter, and T. Wies
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010
  46. Combining Theories with Shared Set Operations pdf slides

    T. Wies, R. Piskac, and V. Kuncak
    In Proceedings of Symposium on Frontiers of Combining Systems (FroCoS), 2009
  47. Abstraction Refinement for Quantified Array Assertions pdf

    M.N. Seghir, A. Podelski, and T. Wies
    In Proceedings of Static Analysis Symposium (SAS), 2009
  48. It's Doomed; We Can Prove It pdf

    J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies
    In Proceedings of Formal Methods (FM), 2009
  49. Intra-module Inference pdf

    S.K. Lahiri, S. Qadeer, J.P. Galeotti, J.W. Voung, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2009
  50. Heap Assumptions on Demand pdf

    A. Podelski, A. Rybalchenko, and T. Wies
    In Proceedings of Computer Aided Verification (CAV), 2008
  51. Shape Analysis for Composite Data Structures pdf

    J. Berdine, C. Calcagno, B. Cook, D. Distefano, P.W. O'Hearn, T. Wies, and H. Yang
    In Proceedings of Computer Aided Verification (CAV), 2007
  52. Using First-Order Theorem Provers in the Jahob Data Structure Verification System pdf

    C. Bouillaguet, V. Kuncak, T. Wies, K. Zee, and M.C. Rinard
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2007
  53. Field Constraint Analysis pdf

    T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard
    In Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI), 2006
  54. Boolean Heaps pdf

    A. Podelski and T. Wies
    In Proceedings of Static Analysis Symposium (SAS), 2005

In Workshops

  1. RECIPE: Applying Open Domain Question Answering to Privacy Policies pdf

    Y. Shvartzshanider, A. Balashankar, T. Wies, and L. Subramanian
    In Proceedings of Workshop on Machine Reading for Question Answering@ACL, 2018
  2. Static Scheduling in Clouds pdf

    T.A. Henzinger, A.V. Singh, V. Singh, T. Wies, and D. Zufferey
    In Proceedings of USENIX Workshop on Hot Topics in Cloud Computing (HotCloud), 2011
  3. (EC)^2 in EC2 pdf

    T.A. Henzinger, A.V. Singh, V. Singh, T. Wies, and D. Zufferey
    In Proceedings of Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2), 2011
  4. Verifying Complex Properties using Symbolic Shape Analysis pdf

    T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard
    In Proceedings of Workshop on Heap Analysis and Verification (HAV), 2007

Thesis

  1. Symbolic Shape Analysis pdf

    T. Wies
    University of Freiburg, Freiburg, Germany, 2009

Technical Reports

  1. Complete Multiparty Session Type Projection with Automata pdf

    E. Li, F. Stutz, T. Wies, and D. Zufferey
    arXiv Technical Report, abs/2305.170792023
  2. Less is more: refinement proofs for probabilistic proofs pdf

    K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, and T. Wies
    IACR Cryptol. ePrint Arch. Technical Report, 2022/15572022
  3. Embedding Hindsight Reasoning in Separation Logic pdf

    R. Meyer, T. Wies, and S. Wolff
    arXiv Technical Report, abs/2209.136922022
  4. A Concurrent Program Logic with a Future and History pdf

    R. Meyer, T. Wies, and S. Wolff
    arXiv Technical Report, arXiv:2207.023552022
  5. Local Reasoning for Global Graph Properties pdf

    S. Krishna, A.J. Summers, and T. Wies
    arXiv Technical Report, arXiv:1911.086322019
  6. Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version) pdf

    S. Krishna, D. Shasha, and T. Wies
    arXiv Technical Report, arXiv:1711.032722017
  7. On Structural Counter Abstraction pdf

    K. Bansal, E. Koskinen, T. Wies, and D. Zufferey
    NYU Technical Report, TR2012-9472013
  8. Automating Separation Logic Using SMT pdf

    R. Piskac, T. Wies, and D. Zufferey
    NYU Technical Report, TR2013-9542013
  9. Complete Instantiation-Based Interpolation pdf

    N. Totla and T. Wies
    NYU Technical Report, TR2012-9502012
  10. On An Efficient Decision Procedure for Imperative Tree Data Structures pdf

    T. Wies, M. Muñiz, and V. Kuncak
    IST Technical Report, IST-2011-00052011
  11. On Deciding Functional Lists with Sublist Sets pdf

    T. Wies, M. Mu\~n, and V. Kuncak
    EPFL Technical Report, EPFL-REPORT-1483612010
  12. On Combining Theories with Shared Set Operations pdf

    T. Wies, R. Piskac, and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-0022009
  13. On Set-Driven Combination of Logics and Verifiers pdf

    T. Wies and V. Kuncak
    EPFL Technical Report, LARA-REPORT-2009-0012009
  14. On Field Constraint Analysis pdf

    T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard
    MIT CSAIL Technical Report, MIT-CSAIL-TR-2005-072, MIT-LCS-TR-10102005